\documentclass{llncs}

\usepackage{url}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}


\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}

\newcommand{\text}[1]{\mbox{#1}}
\newcommand{\wc}{\_}
\newcommand{\mulstep}{ \stackrel{*}{\leadsto}}
\newcommand{\lam}[2]{\lambda #1 . #2}
\newcommand{\evals}[2]{#1 \downarrow #2}

\newcommand{\wm}[0]{\stackrel{\textit{w}}{\to}}
\newcommand{\interp}[1]{[\negthinspace[#1]\negthinspace]}
\newcommand{\symm}[1]{\langle\textit{#1}\rangle}
\newcommand{\rrl}[1]{\textit{r-#1}}
\newcommand{\rrlb}[0]{\textit{r-}\beta}
\newcommand{\trl}[1]{\textit{t-#1}}
\begin{document}
%\pagestyle{empty}
\title{Programming Language in Flat Form}
\author{Peng Fu}
\institute{Independent Project-I}
\date{Nov 18, 2012}


\maketitle
\thispagestyle{empty}



\section{Language Description}

\subsection{Basic Concepts}
\begin{definition}[Terms]

\

\noindent $ t \ ::= \ x \ | \ t t' \ | \ \lambda x.t \ | \ f \ | \ c$.

\end{definition}

\noindent \textbf{Notice:} 

\

\noindent 1. $t$ specify the names/senses of the objects(which can also be function). So we assume the notion of object subsume the notion of function. 

\

\noindent 2. In order to admit higher order functions, we treat function as object.

\

\noindent 3. This specification does not prevent you to have terms like $\lambda x.xx$ .

\

\noindent 4. $f$ is the primitive function sign, can be $+$ sign and others. $c$ is the constant sign, can be $1, 2, ...$. We are not doing philosophy foundation of numbers here, we have to assume certain foundation in order to deal with more practical applications.

\begin{definition}[Individuals]

\

\noindent $ o \ :: =  t \ | \ \iota x. F$


\end{definition}

\begin{definition}[Formula]

\

\noindent $ F \ ::= R(o_1,...,o_n) \ | \ o_1 = o_2 \ | \ o \in (\iota x.F)  \ | \ \forall x.F \ | \ F_1 \to F_2 \ | \ F_1 \wedge F_2 \ | \ \exists x.F \ | \ F_1 \vee F_2 \ | \ \neg F$.

\end{definition}

\subsection{Semantics}
\begin{definition}[Real Entities]

\

\noindent $  \mathbf{N} \ | \ \mathsf{String} \ | \ \mathsf{Bool} $

\end{definition}

\begin{definition}[Evaluation]

\

\noindent $ E \ ::= \ ! t \ | \  ! F $

\end{definition}

\noindent \textbf{Intended Meaning}: $! t$ means evaluating $t$, $! F$ get the truth value of the formula $F$.  

\begin{definition}[Refering/Completion/Assignment]

\

\noindent $ A \ ::=  \ x \leftarrow o \ | \ x \leftarrow E \ | \ x \leftarrow P$.

\end{definition}

\begin{definition}[Commands]

\

\noindent $ L \ ::=  \mathbf{Do}(o_1,..., o_n ) \ | \ A \ |\ \mathbf{if}\ F\ \mathbf{then}\ L \ \mathbf{else}\ L' \ | \ L \ ; \ L' \ | \ \mathbf{for}\  (C;F;C)\ \{L\} \ | \ \mathbf{case}\  t\ \mathbf{of}\ \{t_1 \rightarrow L_1;\ t_2 \to L_2 ;\ ... ;\ t_n \to L_n\}$.

\end{definition}

\noindent $\mathbf{Do}$ is really a shorthand for imperative functions like $\mathbf{print}, \mathbf{return}$ etc. 

\begin{definition}[Program]

\noindent $ P \ ::=  \ \xi x.L \ |  \ \xi y.P$
\end{definition}




\section{Design Principle}


\noindent I treat ``imperitive'' program as function in semantics domain, using refering to bind a variable to a function. Lambda binder give us power to use syntactical combinations to refer to more complex function.  
\section{Module System}

\end{document}
